Halo 2
3.1 Proving System
3.1.1 Lookup argument
AとSは重複を含むことができる。AとSで表される集合が自然に2^kのサイズにならない場合、Sを重複で拡張し、AをSに含まれることが分かっているダミー値で拡張する。
あるいは、A列のどの要素がlookupに含まれるかを制御するlookup selectorを追加することもできる。これは、以下のpermutation rule にあるA(X)の出現を修正し、lookupが選択されない場合、Aを例えばS_0に置き換えるものである。
>S,Aはどちらが長いのか? どちらもadvice columns?圧縮対象であることは間違いない
はi行目で1に評価されるラグランジュ基底多項式であり、それ以外は0である。
証明者はA,Sの並べ替えにより効率的かつ小さいサイズのproofを生成できる。
この時、並べ替えた後のA,SをA',S'とすると、以下のルールで積列Zを持つ順列引数を用いて順列であることを強制することができる。
>ωってなんだっけ?
ここで、分母=0となることはないと仮定すると、全てのに対して一般化すると
これは、A ′とS ′がそれぞれAとSの並べ換えであることを認めるが、正確な並べ換えを指定しない並べ換え論のバージョンである。βとγは別々の課題なので、この2つの並べ換え論が互いに干渉することを心配せずに1つにまとめることができる。
列 A ′のすべてのセルは,同値のセルが垂直に隣接するように配置される.これはある種のソート・アルゴリズムで可能であるが,重要なのは同値のセルが列A ′の連続した行にあること,そしてA ′がAの順列であることである.
>???
A ′の同値の列の最初の行は、S ′の対応する値を持つ行である。この制約を除けば,S ′はSの任意の並べ換えである.
この時、,もしくはを強制するルールを以下のように定義する
また、は以下のルールに従う
の部分は二つ目のルールがあるためrow=0に影響を与えない。
これらの制約を合わせると,A′のすべての要素(つまりA)がS(したがってA)のすべての要素はS ′(したがってS)の少なくとも一つの要素に等しくなるように強制される。
>具体的になんで強制できるんや?
PLONKベースの証明システムで知識ゼロを実現するためには、各列の最後のt行をランダムな値で埋める必要がある。
このようなランダムな値は上述の制約を満たさないため、lookupの引数を調整する必要がある。
まず、使用可能な行数をu=2^k-t-1とする
さらに、二つのセレクターを導入する
q_blind: 最後のtで1になり、それ以外では0になる
q_last:: u行のみ1、それ以外は0に設定される(つまり、使用可能行と目隠し行の中間の行に設定される)。
>uとq_blindの最後の1行って同じじゃね?
使用可能な行に対してのみ、上記の制約を有効にすると
row=0に対しても同様に
でZが再び1になることを保証する回り込みにもはや頼ることができないので、代わりにを1に拘束する必要がある.
ただし、に対してまたはの値のいずれかが0であれば、順列の議論を満たすことができない可能性がある
これはβとγの選択に対して無視できる確率で発生するが、ゼロ知識性と完全性を達成する障害でもある。
完全性とゼロ知識性を保証するために、が0か1であることを許容する。
ここで、もしまたはがあるiについて0である場合、についてと設定でき、制約系を満足することができる。
なお、チャレンジβとγはAとSをコミットした後に選択される(A ′とS ′ にコミットした後に選ばれる)ので、あるまたはが0である場合を、証明者が強制的に発生させることはできない。
このケースは無視できる確率で発生するため、健全性に影響はない。
AとSはランダムチャレンジで組み合わせて複数の列に拡張することができます。A ′とS ′は単一のカラムのままである。
Sのカラムに対するコミットメントは事前に計算され、Pedersen Commitmentの同型性を利用してチャレンジが分かれば安価に結合することができる。
Aの列は相対参照を使って任意の多項式で与えることができる。これらは、最大次数の制限にしたがって、積の列の制約に代入される。これにより、1つ以上のアドバイス列が節約される可能性がある。
すなわち、各行のR(x,y,...)を拘束するために、Rを(前項の方法で)タプルの集合Sとみなし、 (x,y,...)∈R であることを確認すればよい。
Rが関数を表す場合、これは暗黙のうちに入力がドメイン内にあることも チェックする。これは典型的に我々が望むことであり、しばしば追加の範囲チェックを省くことができる。
同じ回路内の複数のテーブルを、元のテーブルを識別するためのタグカラムを含む1つのテーブルにまとめることで、対応できる。
このタグカラムは、先に述べた「ルックアップセレクタ」が実装されれば、統合される可能性がある。
>多項式コミットメントにはPedersen Commitmentを使用する
元の列Aと固定列Sがある。
順列積列Zがある。
2つの順列A ′とS ′がある。
ゲートはすべて低次である。
参考文献